Nuprl Lemma : int_upper_ind
13,42
postcript
pdf
i
:
,
E
:({
i
...}
{u}).
E
(
i
)
(
k
:{
i
+1...}.
E
(
k
- 1)
E
(
k
))
{
k
:{
i
...}.
E
(
k
)}
latex
Up
int
2
,
int
2
Definitions
False
,
A
,
A
B
,
t
T
,
{
T
}
,
x
(
s
)
,
P
Q
,
,
{
i
...}
,
x
:
A
.
B
(
x
)
,
x
.
t
(
x
)
,
WellFnd{i}(
A
;
x
,
y
.
R
(
x
;
y
))
,
P
Q
,
Dec(
P
)
Lemmas
le
wf
,
int
upper
wf
,
int
upper
well
founded
,
decidable
int
equal
origin
i:
, E:({i...}
{u}). E(i) 
(k:{i+1...}. E(k - 1) E(k)) {k:{i...}. E(k)} i:, E:({i...}{u}). E(i) (k:{i+1...}. E(k - 1) E(k)) {k:{i...}. E(k)} 
A
B
T Qx:A. B(x)
x. t(x)
Q